Termination w.r.t. Q proof of /home/nowonder/forschung/aprove/satrung/aprove/lpar3/CimeSLASHquick.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.

Q DP problem:
The TRS P consists of the following rules:

MATCH_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> TEST₂(a_4, x)
MATCH_4₂(l_5, Cons₂(a, l')) -> PART₂(a, l')
APPEND₂(l1_2, l2_1) -> MATCH_0₃(l1_2, l2_1, l1_2)
MATCH_1₃(a_4, l_3, Cons₂(x, l')) -> PART₂(a_4, l')
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> APPEND₂(quick₁(l1), Cons₂(a, quick₁(l2)))
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> QUICK₁(l1)
QUICK₁(l_5) -> MATCH_4₂(l_5, l_5)
MATCH_4₂(l_5, Cons₂(a, l')) -> MATCH_5₄(a, l', l_5, part₂(a, l'))
MATCH_0₃(l1_2, l2_1, Cons₂(x, l)) -> APPEND₂(l, l2_1)
MATCH_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> MATCH_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
MATCH_1₃(a_4, l_3, Cons₂(x, l')) -> MATCH_2₅(x, l', a_4, l_3, part₂(a_4, l'))
PART₂(a_4, l_3) -> MATCH_1₃(a_4, l_3, l_3)
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> QUICK₁(l2)

The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MATCH_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> TEST₂(a_4, x)
MATCH_4₂(l_5, Cons₂(a, l')) -> PART₂(a, l')
APPEND₂(l1_2, l2_1) -> MATCH_0₃(l1_2, l2_1, l1_2)
MATCH_1₃(a_4, l_3, Cons₂(x, l')) -> PART₂(a_4, l')
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> APPEND₂(quick₁(l1), Cons₂(a, quick₁(l2)))
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> QUICK₁(l1)
QUICK₁(l_5) -> MATCH_4₂(l_5, l_5)
MATCH_4₂(l_5, Cons₂(a, l')) -> MATCH_5₄(a, l', l_5, part₂(a, l'))
MATCH_0₃(l1_2, l2_1, Cons₂(x, l)) -> APPEND₂(l, l2_1)
MATCH_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> MATCH_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
MATCH_1₃(a_4, l_3, Cons₂(x, l')) -> MATCH_2₅(x, l', a_4, l_3, part₂(a_4, l'))
PART₂(a_4, l_3) -> MATCH_1₃(a_4, l_3, l_3)
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> QUICK₁(l2)

The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 3 SCCs with 5 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPAfsSolverProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PART₂(a_4, l_3) -> MATCH_1₃(a_4, l_3, l_3)
MATCH_1₃(a_4, l_3, Cons₂(x, l')) -> PART₂(a_4, l')

The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

MATCH_1₃(a_4, l_3, Cons₂(x, l')) -> PART₂(a_4, l')

Used argument filtering: PART₂(x1, x2) = x2
MATCH_1₃(x1, x2, x3) = x3
Cons₂(x1, x2) = Cons₁(x2)
Used ordering: Quasi Precedence: trivial

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPAfsSolverProof

              ↳ QDP

                ↳ DependencyGraphProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PART₂(a_4, l_3) -> MATCH_1₃(a_4, l_3, l_3)

The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 0 SCCs with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MATCH_0₃(l1_2, l2_1, Cons₂(x, l)) -> APPEND₂(l, l2_1)
APPEND₂(l1_2, l2_1) -> MATCH_0₃(l1_2, l2_1, l1_2)

The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

MATCH_0₃(l1_2, l2_1, Cons₂(x, l)) -> APPEND₂(l, l2_1)

Used argument filtering: MATCH_0₃(x1, x2, x3) = x3
Cons₂(x1, x2) = Cons₁(x2)
APPEND₂(x1, x2) = x1
Used ordering: Quasi Precedence: trivial

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

              ↳ QDP

                ↳ DependencyGraphProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APPEND₂(l1_2, l2_1) -> MATCH_0₃(l1_2, l2_1, l1_2)

The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 0 SCCs with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MATCH_4₂(l_5, Cons₂(a, l')) -> MATCH_5₄(a, l', l_5, part₂(a, l'))
QUICK₁(l_5) -> MATCH_4₂(l_5, l_5)
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> QUICK₁(l2)
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> QUICK₁(l1)

The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.